It seems like Any-insertWith-just isn't general enough, which might be related to deprecating with name changes. Not sure if there's a standard practice for how to chose new names when the old lemma isn't general enough, but I thought I'd mention it here.

The problem with Any-insertWith-just is (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))). See that v is not constrained to be the preexisting v in the old tree. So this is good enough to prove Any-insert-just, which ignores the v anyway, but doesn't seem useful when insertWith is used with a non-trivial function.

One possible fix is:

Any-insertWith-just-strong :
  (∀ k′ v → (eq : k ≈ k′) → Q (k′ , v) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
  (q : Any Q t) → k ≈ lookupKey q →
  Any P (proj₂ (insertWith k f t seg))

The proof of this happens to be almost exactly a copy and paste of the existing Any-insertWith-just.

Nice! Thanks very much.
The thing to do in such circumstances would be to fix the type of the 'new' functions, and deprecate the old, but noting that the type has improved. At least if I recall previous episodes of this character... will look properly in the morning soon!

So... I've been thinking about your comment a bit more (but not really doing any proof), and your generalisation, while it seems stronger, perhaps may also be refactored via the existing proof and Properties.Lookup.lookup-rebuild?